The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^3).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^3).


The TRS R consists of the following rules:

terms(N) → cons(recip(sqr(N)))
sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))
dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y)) → cons(Y)

Rewrite Strategy: INNERMOST

(1) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^3).


The TRS R consists of the following rules:

terms(N) → cons(recip(sqr(N))) [1]
sqr(0) → 0 [1]
sqr(s(X)) → s(add(sqr(X), dbl(X))) [1]
dbl(0) → 0 [1]
dbl(s(X)) → s(s(dbl(X))) [1]
add(0, X) → X [1]
add(s(X), Y) → s(add(X, Y)) [1]
first(0, X) → nil [1]
first(s(X), cons(Y)) → cons(Y) [1]

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

terms(N) → cons(recip(sqr(N))) [1]
sqr(0) → 0 [1]
sqr(s(X)) → s(add(sqr(X), dbl(X))) [1]
dbl(0) → 0 [1]
dbl(s(X)) → s(s(dbl(X))) [1]
add(0, X) → X [1]
add(s(X), Y) → s(add(X, Y)) [1]
first(0, X) → nil [1]
first(s(X), cons(Y)) → cons(Y) [1]

The TRS has the following type information:

terms :: 0:s → cons:nil cons :: recip → cons:nil recip :: 0:s → recip sqr :: 0:s → 0:s 0 :: 0:s s :: 0:s → 0:s add :: 0:s → 0:s → 0:s dbl :: 0:s → 0:s first :: 0:s → cons:nil → cons:nil nil :: cons:nil

Rewrite Strategy: INNERMOST

(5) CompletionProof (UPPER BOUND(ID) transformation)

The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:

terms
first

(c) The following functions are completely defined:

sqr
dbl
add

Due to the following rules being added:
none

And the following fresh constants:

const

(6) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: terms(N) → cons(recip(sqr(N))) [1] sqr(0) → 0 [1] sqr(s(X)) → s(add(sqr(X), dbl(X))) [1] dbl(0) → 0 [1] dbl(s(X)) → s(s(dbl(X))) [1] add(0, X) → X [1] add(s(X), Y) → s(add(X, Y)) [1] first(0, X) → nil [1] first(s(X), cons(Y)) → cons(Y) [1] The TRS has the following type information: terms :: 0:s → cons:nil cons :: recip → cons:nil recip :: 0:s → recip sqr :: 0:s → 0:s 0 :: 0:s s :: 0:s → 0:s add :: 0:s → 0:s → 0:s dbl :: 0:s → 0:s first :: 0:s → cons:nil → cons:nil nil :: cons:nil const :: recip Rewrite Strategy: INNERMOST

(7) NarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Narrowed the inner basic terms of all right-hand sides by a single narrowing step.

(8) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: terms(N) → cons(recip(sqr(N))) [1] sqr(0) → 0 [1] sqr(s(0)) → s(add(0, 0)) [3] sqr(s(s(X'))) → s(add(s(add(sqr(X'), dbl(X'))), s(s(dbl(X'))))) [3] dbl(0) → 0 [1] dbl(s(X)) → s(s(dbl(X))) [1] add(0, X) → X [1] add(s(X), Y) → s(add(X, Y)) [1] first(0, X) → nil [1] first(s(X), cons(Y)) → cons(Y) [1] The TRS has the following type information: terms :: 0:s → cons:nil cons :: recip → cons:nil recip :: 0:s → recip sqr :: 0:s → 0:s 0 :: 0:s s :: 0:s → 0:s add :: 0:s → 0:s → 0:s dbl :: 0:s → 0:s first :: 0:s → cons:nil → cons:nil nil :: cons:nil const :: recip Rewrite Strategy: INNERMOST

(9) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

0 => 0
nil => 0
const => 0

(10) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ X :|: z' = X, X >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(X, Y) :|: z = 1 + X, z' = Y, Y >= 0, X >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + (1 + dbl(X)) :|: z = 1 + X, X >= 0
first(z, z') -{ 1 }→ 0 :|: z' = X, X >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y :|: z = 1 + X, Y >= 0, z' = 1 + Y, X >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 3 }→ 1 + add(1 + add(sqr(X'), dbl(X')), 1 + (1 + dbl(X'))) :|: X' >= 0, z = 1 + (1 + X')
terms(z) -{ 1 }→ 1 + (1 + sqr(N)) :|: z = N, N >= 0

(11) SimplificationProof (BOTH BOUNDS(ID, ID) transformation)

Simplified the RNTS by moving equalities from the constraints into the right-hand sides.

(12) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 3 }→ 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) :|: z >= 0

(13) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID) transformation)

Found the following analysis order by SCC decomposition:

{ first } { dbl } { add } { sqr } { terms }

(14) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 3 }→ 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) :|: z >= 0

Function symbols to be analyzed: {first}, {dbl}, {add}, {sqr}, {terms}

(15) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: first
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z'

(16) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 3 }→ 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) :|: z >= 0

Function symbols to be analyzed: {first}, {dbl}, {add}, {sqr}, {terms}
Previous analysis results are:

first: runtime: ?, size: O(n1) [z']

(17) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: first
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(18) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 3 }→ 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) :|: z >= 0

Function symbols to be analyzed: {dbl}, {add}, {sqr}, {terms}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [z']

(19) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(20) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 3 }→ 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) :|: z >= 0

Function symbols to be analyzed: {dbl}, {add}, {sqr}, {terms}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [z']

(21) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: dbl
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 2·z

(22) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 3 }→ 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) :|: z >= 0

Function symbols to be analyzed: {dbl}, {add}, {sqr}, {terms}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [z'] dbl: runtime: ?, size: O(n1) [2·z]

(23) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: dbl
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(24) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 3 }→ 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) :|: z >= 0

Function symbols to be analyzed: {add}, {sqr}, {terms}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [z'] dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z]

(25) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(26) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s), 1 + (1 + s')) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) :|: z >= 0

Function symbols to be analyzed: {add}, {sqr}, {terms}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [z'] dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z]

(27) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: add
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z + z'

(28) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s), 1 + (1 + s')) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) :|: z >= 0

Function symbols to be analyzed: {add}, {sqr}, {terms}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [z'] dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: ?, size: O(n1) [z + z']

(29) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: add
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(30) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s), 1 + (1 + s')) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) :|: z >= 0

Function symbols to be analyzed: {sqr}, {terms}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [z'] dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z']

(31) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(32) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s), 1 + (1 + s')) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) :|: z >= 0

Function symbols to be analyzed: {sqr}, {terms}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [z'] dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z']

(33) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: sqr
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 1 + 4·z + 4·z²

(34) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s), 1 + (1 + s')) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) :|: z >= 0

Function symbols to be analyzed: {sqr}, {terms}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [z'] dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] sqr: runtime: ?, size: O(n2) [1 + 4·z + 4·z2]

(35) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: sqr
after applying outer abstraction to obtain an ITS,
resulting in: O(n³) with polynomial bound: 5 + 22·z + 8·z³

(36) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s), 1 + (1 + s')) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) :|: z >= 0

Function symbols to be analyzed: {terms}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [z'] dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] sqr: runtime: O(n3) [5 + 22·z + 8·z3], size: O(n2) [1 + 4·z + 4·z2]

(37) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(38) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ -99 + s4 + s5 + 120·z + -48·z² + 8·z³ }→ 1 + s6 :|: s4 >= 0, s4 <= 4 * ((z - 2) * (z - 2)) + 4 * (z - 2) + 1, s5 >= 0, s5 <= 1 * s4 + 1 * s, s6 >= 0, s6 <= 1 * (1 + s5) + 1 * (1 + (1 + s')), s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 6 + 22·z + 8·z³ }→ 1 + (1 + s3) :|: s3 >= 0, s3 <= 4 * (z * z) + 4 * z + 1, z >= 0

Function symbols to be analyzed: {terms}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [z'] dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] sqr: runtime: O(n3) [5 + 22·z + 8·z3], size: O(n2) [1 + 4·z + 4·z2]

(39) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: terms
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 3 + 4·z + 4·z²

(40) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ -99 + s4 + s5 + 120·z + -48·z² + 8·z³ }→ 1 + s6 :|: s4 >= 0, s4 <= 4 * ((z - 2) * (z - 2)) + 4 * (z - 2) + 1, s5 >= 0, s5 <= 1 * s4 + 1 * s, s6 >= 0, s6 <= 1 * (1 + s5) + 1 * (1 + (1 + s')), s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 6 + 22·z + 8·z³ }→ 1 + (1 + s3) :|: s3 >= 0, s3 <= 4 * (z * z) + 4 * z + 1, z >= 0

Function symbols to be analyzed: {terms}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [z'] dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] sqr: runtime: O(n3) [5 + 22·z + 8·z3], size: O(n2) [1 + 4·z + 4·z2] terms: runtime: ?, size: O(n2) [3 + 4·z + 4·z2]

(41) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: terms
after applying outer abstraction to obtain an ITS,
resulting in: O(n³) with polynomial bound: 6 + 22·z + 8·z³

(42) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ -99 + s4 + s5 + 120·z + -48·z² + 8·z³ }→ 1 + s6 :|: s4 >= 0, s4 <= 4 * ((z - 2) * (z - 2)) + 4 * (z - 2) + 1, s5 >= 0, s5 <= 1 * s4 + 1 * s, s6 >= 0, s6 <= 1 * (1 + s5) + 1 * (1 + (1 + s')), s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 6 + 22·z + 8·z³ }→ 1 + (1 + s3) :|: s3 >= 0, s3 <= 4 * (z * z) + 4 * z + 1, z >= 0

Function symbols to be analyzed:
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [z'] dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] sqr: runtime: O(n3) [5 + 22·z + 8·z3], size: O(n2) [1 + 4·z + 4·z2] terms: runtime: O(n3) [6 + 22·z + 8·z3], size: O(n2) [3 + 4·z + 4·z2]

(43) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity

(44) BOUNDS(1, n^3)